Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

+(0, 0) → 0
+(0, 1) → 1
+(0, 2) → 2
+(0, 3) → 3
+(0, 4) → 4
+(0, 5) → 5
+(0, 6) → 6
+(0, 7) → 7
+(0, 8) → 8
+(0, 9) → 9
+(1, 0) → 1
+(1, 1) → 2
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 8) → c(1, 0)
+(2, 9) → c(1, 1)
+(3, 0) → 3
+(3, 1) → 4
+(3, 2) → 5
+(3, 3) → 6
+(3, 4) → 7
+(3, 5) → 8
+(3, 6) → 9
+(3, 7) → c(1, 0)
+(3, 8) → c(1, 1)
+(3, 9) → c(1, 2)
+(4, 0) → 4
+(4, 1) → 5
+(4, 2) → 6
+(4, 3) → 7
+(4, 4) → 8
+(4, 5) → 9
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(5, 0) → 5
+(5, 1) → 6
+(5, 2) → 7
+(5, 3) → 8
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(6, 0) → 6
+(6, 1) → 7
+(6, 2) → 8
+(6, 3) → 9
+(6, 4) → c(1, 0)
+(6, 5) → c(1, 1)
+(6, 6) → c(1, 2)
+(6, 7) → c(1, 3)
+(6, 8) → c(1, 4)
+(6, 9) → c(1, 5)
+(7, 0) → 7
+(7, 1) → 8
+(7, 2) → 9
+(7, 3) → c(1, 0)
+(7, 4) → c(1, 1)
+(7, 5) → c(1, 2)
+(7, 6) → c(1, 3)
+(7, 7) → c(1, 4)
+(7, 8) → c(1, 5)
+(7, 9) → c(1, 6)
+(8, 0) → 8
+(8, 1) → 9
+(8, 2) → c(1, 0)
+(8, 3) → c(1, 1)
+(8, 4) → c(1, 2)
+(8, 5) → c(1, 3)
+(8, 6) → c(1, 4)
+(8, 7) → c(1, 5)
+(8, 8) → c(1, 6)
+(8, 9) → c(1, 7)
+(9, 0) → 9
+(9, 1) → c(1, 0)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

+(0, 0) → 0
+(0, 1) → 1
+(0, 2) → 2
+(0, 3) → 3
+(0, 4) → 4
+(0, 5) → 5
+(0, 6) → 6
+(0, 7) → 7
+(0, 8) → 8
+(0, 9) → 9
+(1, 0) → 1
+(1, 1) → 2
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 8) → c(1, 0)
+(2, 9) → c(1, 1)
+(3, 0) → 3
+(3, 1) → 4
+(3, 2) → 5
+(3, 3) → 6
+(3, 4) → 7
+(3, 5) → 8
+(3, 6) → 9
+(3, 7) → c(1, 0)
+(3, 8) → c(1, 1)
+(3, 9) → c(1, 2)
+(4, 0) → 4
+(4, 1) → 5
+(4, 2) → 6
+(4, 3) → 7
+(4, 4) → 8
+(4, 5) → 9
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(5, 0) → 5
+(5, 1) → 6
+(5, 2) → 7
+(5, 3) → 8
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(6, 0) → 6
+(6, 1) → 7
+(6, 2) → 8
+(6, 3) → 9
+(6, 4) → c(1, 0)
+(6, 5) → c(1, 1)
+(6, 6) → c(1, 2)
+(6, 7) → c(1, 3)
+(6, 8) → c(1, 4)
+(6, 9) → c(1, 5)
+(7, 0) → 7
+(7, 1) → 8
+(7, 2) → 9
+(7, 3) → c(1, 0)
+(7, 4) → c(1, 1)
+(7, 5) → c(1, 2)
+(7, 6) → c(1, 3)
+(7, 7) → c(1, 4)
+(7, 8) → c(1, 5)
+(7, 9) → c(1, 6)
+(8, 0) → 8
+(8, 1) → 9
+(8, 2) → c(1, 0)
+(8, 3) → c(1, 1)
+(8, 4) → c(1, 2)
+(8, 5) → c(1, 3)
+(8, 6) → c(1, 4)
+(8, 7) → c(1, 5)
+(8, 8) → c(1, 6)
+(8, 9) → c(1, 7)
+(9, 0) → 9
+(9, 1) → c(1, 0)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

+1(7, 4) → C(1, 1)
+1(6, 5) → C(1, 1)
+1(2, 9) → C(1, 1)
+1(3, 8) → C(1, 1)
+1(4, 7) → C(1, 1)
+1(5, 6) → C(1, 1)
+1(8, 3) → C(1, 1)
+1(9, 2) → C(1, 1)
+1(x, c(y, z)) → +1(x, z)
C(x, c(y, z)) → C(+(x, y), z)
+1(6, 9) → C(1, 5)
+1(7, 8) → C(1, 5)
+1(8, 7) → C(1, 5)
+1(9, 6) → C(1, 5)
+1(6, 8) → C(1, 4)
+1(5, 9) → C(1, 4)
+1(7, 7) → C(1, 4)
+1(8, 6) → C(1, 4)
+1(9, 5) → C(1, 4)
+1(c(x, y), z) → +1(y, z)
+1(7, 9) → C(1, 6)
+1(8, 8) → C(1, 6)
+1(9, 7) → C(1, 6)
+1(7, 3) → C(1, 0)
+1(6, 4) → C(1, 0)
+1(1, 9) → C(1, 0)
+1(2, 8) → C(1, 0)
+1(3, 7) → C(1, 0)
+1(4, 6) → C(1, 0)
+1(5, 5) → C(1, 0)
+1(8, 2) → C(1, 0)
+1(9, 1) → C(1, 0)
C(x, c(y, z)) → +1(x, y)
+1(9, 9) → C(1, 8)
+1(x, c(y, z)) → C(y, +(x, z))
+1(7, 6) → C(1, 3)
+1(6, 7) → C(1, 3)
+1(5, 8) → C(1, 3)
+1(4, 9) → C(1, 3)
+1(8, 5) → C(1, 3)
+1(9, 4) → C(1, 3)
+1(7, 5) → C(1, 2)
+1(6, 6) → C(1, 2)
+1(3, 9) → C(1, 2)
+1(4, 8) → C(1, 2)
+1(5, 7) → C(1, 2)
+1(8, 4) → C(1, 2)
+1(9, 3) → C(1, 2)
+1(c(x, y), z) → C(x, +(y, z))
+1(8, 9) → C(1, 7)
+1(9, 8) → C(1, 7)

The TRS R consists of the following rules:

+(0, 0) → 0
+(0, 1) → 1
+(0, 2) → 2
+(0, 3) → 3
+(0, 4) → 4
+(0, 5) → 5
+(0, 6) → 6
+(0, 7) → 7
+(0, 8) → 8
+(0, 9) → 9
+(1, 0) → 1
+(1, 1) → 2
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 8) → c(1, 0)
+(2, 9) → c(1, 1)
+(3, 0) → 3
+(3, 1) → 4
+(3, 2) → 5
+(3, 3) → 6
+(3, 4) → 7
+(3, 5) → 8
+(3, 6) → 9
+(3, 7) → c(1, 0)
+(3, 8) → c(1, 1)
+(3, 9) → c(1, 2)
+(4, 0) → 4
+(4, 1) → 5
+(4, 2) → 6
+(4, 3) → 7
+(4, 4) → 8
+(4, 5) → 9
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(5, 0) → 5
+(5, 1) → 6
+(5, 2) → 7
+(5, 3) → 8
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(6, 0) → 6
+(6, 1) → 7
+(6, 2) → 8
+(6, 3) → 9
+(6, 4) → c(1, 0)
+(6, 5) → c(1, 1)
+(6, 6) → c(1, 2)
+(6, 7) → c(1, 3)
+(6, 8) → c(1, 4)
+(6, 9) → c(1, 5)
+(7, 0) → 7
+(7, 1) → 8
+(7, 2) → 9
+(7, 3) → c(1, 0)
+(7, 4) → c(1, 1)
+(7, 5) → c(1, 2)
+(7, 6) → c(1, 3)
+(7, 7) → c(1, 4)
+(7, 8) → c(1, 5)
+(7, 9) → c(1, 6)
+(8, 0) → 8
+(8, 1) → 9
+(8, 2) → c(1, 0)
+(8, 3) → c(1, 1)
+(8, 4) → c(1, 2)
+(8, 5) → c(1, 3)
+(8, 6) → c(1, 4)
+(8, 7) → c(1, 5)
+(8, 8) → c(1, 6)
+(8, 9) → c(1, 7)
+(9, 0) → 9
+(9, 1) → c(1, 0)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

+1(7, 4) → C(1, 1)
+1(6, 5) → C(1, 1)
+1(2, 9) → C(1, 1)
+1(3, 8) → C(1, 1)
+1(4, 7) → C(1, 1)
+1(5, 6) → C(1, 1)
+1(8, 3) → C(1, 1)
+1(9, 2) → C(1, 1)
+1(x, c(y, z)) → +1(x, z)
C(x, c(y, z)) → C(+(x, y), z)
+1(6, 9) → C(1, 5)
+1(7, 8) → C(1, 5)
+1(8, 7) → C(1, 5)
+1(9, 6) → C(1, 5)
+1(6, 8) → C(1, 4)
+1(5, 9) → C(1, 4)
+1(7, 7) → C(1, 4)
+1(8, 6) → C(1, 4)
+1(9, 5) → C(1, 4)
+1(c(x, y), z) → +1(y, z)
+1(7, 9) → C(1, 6)
+1(8, 8) → C(1, 6)
+1(9, 7) → C(1, 6)
+1(7, 3) → C(1, 0)
+1(6, 4) → C(1, 0)
+1(1, 9) → C(1, 0)
+1(2, 8) → C(1, 0)
+1(3, 7) → C(1, 0)
+1(4, 6) → C(1, 0)
+1(5, 5) → C(1, 0)
+1(8, 2) → C(1, 0)
+1(9, 1) → C(1, 0)
C(x, c(y, z)) → +1(x, y)
+1(9, 9) → C(1, 8)
+1(x, c(y, z)) → C(y, +(x, z))
+1(7, 6) → C(1, 3)
+1(6, 7) → C(1, 3)
+1(5, 8) → C(1, 3)
+1(4, 9) → C(1, 3)
+1(8, 5) → C(1, 3)
+1(9, 4) → C(1, 3)
+1(7, 5) → C(1, 2)
+1(6, 6) → C(1, 2)
+1(3, 9) → C(1, 2)
+1(4, 8) → C(1, 2)
+1(5, 7) → C(1, 2)
+1(8, 4) → C(1, 2)
+1(9, 3) → C(1, 2)
+1(c(x, y), z) → C(x, +(y, z))
+1(8, 9) → C(1, 7)
+1(9, 8) → C(1, 7)

The TRS R consists of the following rules:

+(0, 0) → 0
+(0, 1) → 1
+(0, 2) → 2
+(0, 3) → 3
+(0, 4) → 4
+(0, 5) → 5
+(0, 6) → 6
+(0, 7) → 7
+(0, 8) → 8
+(0, 9) → 9
+(1, 0) → 1
+(1, 1) → 2
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 8) → c(1, 0)
+(2, 9) → c(1, 1)
+(3, 0) → 3
+(3, 1) → 4
+(3, 2) → 5
+(3, 3) → 6
+(3, 4) → 7
+(3, 5) → 8
+(3, 6) → 9
+(3, 7) → c(1, 0)
+(3, 8) → c(1, 1)
+(3, 9) → c(1, 2)
+(4, 0) → 4
+(4, 1) → 5
+(4, 2) → 6
+(4, 3) → 7
+(4, 4) → 8
+(4, 5) → 9
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(5, 0) → 5
+(5, 1) → 6
+(5, 2) → 7
+(5, 3) → 8
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(6, 0) → 6
+(6, 1) → 7
+(6, 2) → 8
+(6, 3) → 9
+(6, 4) → c(1, 0)
+(6, 5) → c(1, 1)
+(6, 6) → c(1, 2)
+(6, 7) → c(1, 3)
+(6, 8) → c(1, 4)
+(6, 9) → c(1, 5)
+(7, 0) → 7
+(7, 1) → 8
+(7, 2) → 9
+(7, 3) → c(1, 0)
+(7, 4) → c(1, 1)
+(7, 5) → c(1, 2)
+(7, 6) → c(1, 3)
+(7, 7) → c(1, 4)
+(7, 8) → c(1, 5)
+(7, 9) → c(1, 6)
+(8, 0) → 8
+(8, 1) → 9
+(8, 2) → c(1, 0)
+(8, 3) → c(1, 1)
+(8, 4) → c(1, 2)
+(8, 5) → c(1, 3)
+(8, 6) → c(1, 4)
+(8, 7) → c(1, 5)
+(8, 8) → c(1, 6)
+(8, 9) → c(1, 7)
+(9, 0) → 9
+(9, 1) → c(1, 0)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 45 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

C(x, c(y, z)) → +1(x, y)
+1(x, c(y, z)) → C(y, +(x, z))
+1(c(x, y), z) → +1(y, z)
+1(x, c(y, z)) → +1(x, z)
C(x, c(y, z)) → C(+(x, y), z)
+1(c(x, y), z) → C(x, +(y, z))

The TRS R consists of the following rules:

+(0, 0) → 0
+(0, 1) → 1
+(0, 2) → 2
+(0, 3) → 3
+(0, 4) → 4
+(0, 5) → 5
+(0, 6) → 6
+(0, 7) → 7
+(0, 8) → 8
+(0, 9) → 9
+(1, 0) → 1
+(1, 1) → 2
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 8) → c(1, 0)
+(2, 9) → c(1, 1)
+(3, 0) → 3
+(3, 1) → 4
+(3, 2) → 5
+(3, 3) → 6
+(3, 4) → 7
+(3, 5) → 8
+(3, 6) → 9
+(3, 7) → c(1, 0)
+(3, 8) → c(1, 1)
+(3, 9) → c(1, 2)
+(4, 0) → 4
+(4, 1) → 5
+(4, 2) → 6
+(4, 3) → 7
+(4, 4) → 8
+(4, 5) → 9
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(5, 0) → 5
+(5, 1) → 6
+(5, 2) → 7
+(5, 3) → 8
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(6, 0) → 6
+(6, 1) → 7
+(6, 2) → 8
+(6, 3) → 9
+(6, 4) → c(1, 0)
+(6, 5) → c(1, 1)
+(6, 6) → c(1, 2)
+(6, 7) → c(1, 3)
+(6, 8) → c(1, 4)
+(6, 9) → c(1, 5)
+(7, 0) → 7
+(7, 1) → 8
+(7, 2) → 9
+(7, 3) → c(1, 0)
+(7, 4) → c(1, 1)
+(7, 5) → c(1, 2)
+(7, 6) → c(1, 3)
+(7, 7) → c(1, 4)
+(7, 8) → c(1, 5)
+(7, 9) → c(1, 6)
+(8, 0) → 8
+(8, 1) → 9
+(8, 2) → c(1, 0)
+(8, 3) → c(1, 1)
+(8, 4) → c(1, 2)
+(8, 5) → c(1, 3)
+(8, 6) → c(1, 4)
+(8, 7) → c(1, 5)
+(8, 8) → c(1, 6)
+(8, 9) → c(1, 7)
+(9, 0) → 9
+(9, 1) → c(1, 0)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


C(x, c(y, z)) → +1(x, y)
+1(x, c(y, z)) → C(y, +(x, z))
+1(c(x, y), z) → +1(y, z)
+1(x, c(y, z)) → +1(x, z)
C(x, c(y, z)) → C(+(x, y), z)
The remaining pairs can at least be oriented weakly.

+1(c(x, y), z) → C(x, +(y, z))
Used ordering: Polynomial interpretation [25,35]:

POL(7) = 3   
POL(C(x1, x2)) = 4 + (4)x_1 + (2)x_2   
POL(3) = 2   
POL(c(x1, x2)) = 1 + (2)x_1 + x_2   
POL(2) = 1   
POL(6) = 3   
POL(0) = 0   
POL(+1(x1, x2)) = 1 + (3)x_1 + (4)x_2   
POL(+(x1, x2)) = x_1 + x_2   
POL(5) = 2   
POL(9) = 4   
POL(4) = 2   
POL(8) = 4   
POL(1) = 1   
The value of delta used in the strict ordering is 1.
The following usable rules [17] were oriented:

+(0, 3) → 3
+(0, 2) → 2
+(0, 1) → 1
+(0, 0) → 0
+(0, 7) → 7
+(0, 6) → 6
+(0, 5) → 5
+(0, 4) → 4
+(1, 1) → 2
+(1, 0) → 1
+(0, 9) → 9
+(0, 8) → 8
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(3, 3) → 6
+(3, 2) → 5
+(3, 5) → 8
+(3, 4) → 7
+(2, 9) → c(1, 1)
+(2, 8) → c(1, 0)
+(3, 1) → 4
+(3, 0) → 3
+(4, 1) → 5
+(4, 0) → 4
+(4, 3) → 7
+(4, 2) → 6
+(3, 7) → c(1, 0)
+(3, 6) → 9
+(3, 9) → c(1, 2)
+(3, 8) → c(1, 1)
+(5, 0) → 5
+(5, 1) → 6
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 4) → 8
+(4, 5) → 9
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 2) → 7
+(5, 3) → 8
+(6, 7) → c(1, 3)
+(6, 6) → c(1, 2)
+(6, 5) → c(1, 1)
+(6, 4) → c(1, 0)
+(6, 3) → 9
+(6, 2) → 8
+(6, 1) → 7
+(6, 0) → 6
+(7, 5) → c(1, 2)
+(7, 4) → c(1, 1)
+(7, 3) → c(1, 0)
+(7, 2) → 9
+(7, 1) → 8
+(7, 0) → 7
+(6, 9) → c(1, 5)
+(6, 8) → c(1, 4)
+(8, 5) → c(1, 3)
+(8, 4) → c(1, 2)
+(8, 7) → c(1, 5)
+(8, 6) → c(1, 4)
+(8, 9) → c(1, 7)
+(8, 8) → c(1, 6)
+(9, 1) → c(1, 0)
+(9, 0) → 9
+(7, 7) → c(1, 4)
+(7, 6) → c(1, 3)
+(7, 9) → c(1, 6)
+(7, 8) → c(1, 5)
+(8, 1) → 9
+(8, 0) → 8
+(8, 3) → c(1, 1)
+(8, 2) → c(1, 0)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ QDP
          ↳ QDPOrderProof
            ↳ QDP
              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

+1(c(x, y), z) → C(x, +(y, z))

The TRS R consists of the following rules:

+(0, 0) → 0
+(0, 1) → 1
+(0, 2) → 2
+(0, 3) → 3
+(0, 4) → 4
+(0, 5) → 5
+(0, 6) → 6
+(0, 7) → 7
+(0, 8) → 8
+(0, 9) → 9
+(1, 0) → 1
+(1, 1) → 2
+(1, 2) → 3
+(1, 3) → 4
+(1, 4) → 5
+(1, 5) → 6
+(1, 6) → 7
+(1, 7) → 8
+(1, 8) → 9
+(1, 9) → c(1, 0)
+(2, 0) → 2
+(2, 1) → 3
+(2, 2) → 4
+(2, 3) → 5
+(2, 4) → 6
+(2, 5) → 7
+(2, 6) → 8
+(2, 7) → 9
+(2, 8) → c(1, 0)
+(2, 9) → c(1, 1)
+(3, 0) → 3
+(3, 1) → 4
+(3, 2) → 5
+(3, 3) → 6
+(3, 4) → 7
+(3, 5) → 8
+(3, 6) → 9
+(3, 7) → c(1, 0)
+(3, 8) → c(1, 1)
+(3, 9) → c(1, 2)
+(4, 0) → 4
+(4, 1) → 5
+(4, 2) → 6
+(4, 3) → 7
+(4, 4) → 8
+(4, 5) → 9
+(4, 6) → c(1, 0)
+(4, 7) → c(1, 1)
+(4, 8) → c(1, 2)
+(4, 9) → c(1, 3)
+(5, 0) → 5
+(5, 1) → 6
+(5, 2) → 7
+(5, 3) → 8
+(5, 4) → 9
+(5, 5) → c(1, 0)
+(5, 6) → c(1, 1)
+(5, 7) → c(1, 2)
+(5, 8) → c(1, 3)
+(5, 9) → c(1, 4)
+(6, 0) → 6
+(6, 1) → 7
+(6, 2) → 8
+(6, 3) → 9
+(6, 4) → c(1, 0)
+(6, 5) → c(1, 1)
+(6, 6) → c(1, 2)
+(6, 7) → c(1, 3)
+(6, 8) → c(1, 4)
+(6, 9) → c(1, 5)
+(7, 0) → 7
+(7, 1) → 8
+(7, 2) → 9
+(7, 3) → c(1, 0)
+(7, 4) → c(1, 1)
+(7, 5) → c(1, 2)
+(7, 6) → c(1, 3)
+(7, 7) → c(1, 4)
+(7, 8) → c(1, 5)
+(7, 9) → c(1, 6)
+(8, 0) → 8
+(8, 1) → 9
+(8, 2) → c(1, 0)
+(8, 3) → c(1, 1)
+(8, 4) → c(1, 2)
+(8, 5) → c(1, 3)
+(8, 6) → c(1, 4)
+(8, 7) → c(1, 5)
+(8, 8) → c(1, 6)
+(8, 9) → c(1, 7)
+(9, 0) → 9
+(9, 1) → c(1, 0)
+(9, 2) → c(1, 1)
+(9, 3) → c(1, 2)
+(9, 4) → c(1, 3)
+(9, 5) → c(1, 4)
+(9, 6) → c(1, 5)
+(9, 7) → c(1, 6)
+(9, 8) → c(1, 7)
+(9, 9) → c(1, 8)
+(x, c(y, z)) → c(y, +(x, z))
+(c(x, y), z) → c(x, +(y, z))
c(0, x) → x
c(x, c(y, z)) → c(+(x, y), z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.